\section{Types}


\pII{
\begin{quote}
%
%%%%%%%%%%%%%%%%%% State and Declaration Types %%%%%%%%%%%%%%%%%%%%%
%
\ntermdef{StateTypeBinding}
%
\defspace <: \nterm{StateType}
%
\defspace = \nterm{StateType}
%
%
\ntermdef{StateType}
%
\defspace \nterm{StateTypePrim} \seq{\keyw{with} \nterm{StateTypePrim}} % left-associative
%
\ntermdef{StateTypePrim}
%
\defspace \nterm{QualifiedIdentifier} \opt{<\nterm{PermBindingList}>} \opt{\{ \nterm{RenameList} \}}
%
\defspace \{ \seq{\nterm{DeclType}} \}
%
\defspace \keyw{requires} \nterm{StateTypePrim}
%
\end{quote}
}

\pII{Interface definitions are analogous to state definitions, except that
the primitive declaration block gives only declaration types.  In
addition, interfaces can require whole other interfaces or blocks;
this is semantically equivalent to requiring each member in the
specified required interface.
%
\begin{quote}
%
\ntermdef{DeclType}
%
\defspace \seq{\nterm{Modifier}} \keyw{state} \nterm{Identifier}
          \opt{\keyw{case} \keyw{of} \nterm{QualifiedIdentifier}}
          \opt{\nterm{StateTypeBinding}}
%
\defspace \seq{\nterm{Modifier}} \keyw{interface} \nterm{Identifier}
          \opt{\keyw{case} \keyw{of} \nterm{QualifiedIdentifier}}
          \opt{\nterm{StateTypeBinding}}
%
\defspace \seq{\nterm{Modifier}} \keyw{type} \nterm{Identifier}
          \opt{\nterm{TypeDef}}
%
\defspace \seq{\nterm{Modifier}} \seq{\nterm{MSpec}}
%
\defspace \seq{\nterm{Modifier}} \nterm{Type} \nterm{Identifier}
%
\end{quote}
%
These are analogous to full declarations, except that states cannot be
given definitions, only types; methods cannot be given bodies; and
fields cannot be given initial values.
}

%%%%%%%%%%%%%%%%%% Typedefs %%%%%%%%%%%%%%%%%%%%%

\begin{quote}

\pII{
\ntermdef{TypeDef}
%
\defspace = \nterm{Type}
%
\defspace <: \nterm{Type}
}

\ntermdef{Type}

\defspace \nterm{ArgSpecs} \opt{[ \nterm{Args}]} -> \nterm{Type}

\defspace \nterm{QualifiedIdentifier}

\defspace \opt{\nterm{PermKind}} \nterm{State}\pII{\opt{@\nterm{State}}}

\defspace \keyw{none}

\defspace \keyw{dynamic}

\defspace (\nterm{Type})


\ntermdef{PermKind}

\defspace \keyw{unique}

\defspace \keyw{full}

\defspace \keyw{shared}

\defspace \keyw{pure}

\defspace \keyw{immutable}

\vII{\ntermdef{ArgSpecs}}

\vII{\defspace \nterm{ArgSpec} \seq{ * \nterm{ArgSpec} }}



\end{quote}

\pII{Type bindings can be either a definition or a lower bound, just like
interface and state bindings.  Types can be defined as a function
type, a reference to another type definition, or a combination of
permission and state.  It is also possible to have no permission at
all.}

Function types include optional arguments in brackets [] that specify
permissions to objects in scope, along with their state transitions.
\nterm{ArgSpecs} include just the permission and the state, while
\nterm{Args} includes the variable name as well (since for the optional
arguments we are naming variables currently in scope). The arrow operator (->) is right associative. Left associativity is supported by enclosing a \nterm{Type} in parentheses.

\vII{Formally, a function that accepts multiple arguments actually accepts an
argument tuple, which is written with a \code{*}-separated list.}


State types include an optional permission kind, which defaults to the permission kind of the state, or \keyw{dyn} otherwise.
\pII{The optional @ state is for \keyw{full}, \keyw{shared}, and \keyw{pure}, for which the first state given
is the state guarantee and the second state given is the current state,
which defaults to the state guarantee if missing.}

%Permission kinds are the 5 kinds from the Plural system, with the
%semantics described there.  \TODO{re-summarize}


